We present a static analysis by Abstract Interpretation to check for run-timeerrors in parallel and multi-threaded C programs. Following our work onAstr\'ee, we focus on embedded critical programs without recursion nor dynamicmemory allocation, but extend the analysis to a static set of threadscommunicating implicitly through a shared memory and explicitly using a finiteset of mutual exclusion locks, and scheduled according to a real-timescheduling policy and fixed priorities. Our method is thread-modular. It isbased on a slightly modified non-parallel analysis that, when analyzing athread, applies and enriches an abstract set of thread interferences. Aniterator then re-analyzes each thread in turn until interferences stabilize. Weprove the soundness of our method with respect to the sequential consistencysemantics, but also with respect to a reasonable weakly consistent memorysemantics. We also show how to take into account mutual exclusion and threadpriorities through a partitioning over an abstraction of the scheduler state.We present preliminary experimental results analyzing an industrial programwith our prototype, Th\'es\'ee, and demonstrate the scalability of ourapproach.
展开▼
